Nuprl Lemma : binomial_q
11,40
postcript
pdf
a
,
b
:
,
n
:
.
a
+
b
n
=
0
i
<
n
+1. choose(
n
;
i
)
<
+*> (
a
i
*
b
n
-
i
)
latex
Definitions
t
T
,
t
.2
,
t
.1
,
*
,
+
r
,
x
f
y
,
|
r
|
,
<
+*>
,
x
:
A
.
B
(
x
)
,
a
j
<
b
.
E
(
j
)
,
r
n
Lemmas
qrng
wf
,
binomial
origin
a, b:
, n:
. a + b 
n = 
0 
i < n+1. choose(n;i) 
<+*> (a i * b n - i) 
a, b:, n:. a + b n = 0 i < n+1. choose(n;i) <+*> (a i * b n - i) T+*>x:A. B(x)a j < b. E(j) n